perm filename PROVE1.NEW[1,JRA]5 blob
sn#055946 filedate 1973-08-01 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP NEWPROOF
00400 (NIL NEWPROOF
00500 ALLPOS
00600 ALLNEG
00700 ANCESTOR
00800 SEARCH1
00900 CONST
01000 HERE
01100 VAR
01600 MKWRD
01700 NEG
01800 NEGBIT
01900 POS
02000 POSBIT
02100 SEARCH
02200 NUM
02300 NEGL
02400 APPENDIT
02500 ANDOR
02600 ASSOC1
02700 ATTEMPT
02800 AUTO
03000 BAKSUB
03100 BOOKEEP
03200 BUILTED
03300 BUILTED1
03400 BUILTCH
03500 BUILTCH1
03600 CHOICE
03700 CHOICE1
03800 CLAUSES
03900 CLAUSES2
04000 CLAUSES1
04100 CNF
04200 CNF1
04300 CNF2
04400 CNF3
04500 CNVT
04600 CNVT2
04700 CNVT3
04800 COPY
04900 COPYDELETED
05000 *CL
05100 DEMOD
05200 DEM
05300 DEPTH
05400 DEPTH1
05450 DEP DEP1
05500 DEL
05800 DOWN
05900 EDIT
06000 ERPRINT
06100 ERPRIN1
06200 EXPUNGE
06300 FINI
06400 FIXNEG
06500 FIXQFF
06600 FIXQFF1
06700 GENSKOLEM
06800 GETNAME
06900 GETTERMS
07000 GETVARS
07100 GOLIST
07200 INCLAUSES
07300 INITIAL
07400 INITIALAX
07500 INITIALAX1
07600 MAKVAR
07700 MAKOVAR
07800 MAPIT
08500 MAX
08600 MAXDEPTH MAXDEPTH1 MAXLENGTH
08700 MEMC
08800 MIN1
08900 MINIMIZE
09000 MIN
09100 MKSYM
09200 MODEL
09300 NCONC1
09400 NEGATE
09500 NEGSGN
09900 ONEGSGN
10000 *NOPOINT
10100 OCCUR
10200 ORDER
10300 ORDEREQUAL
10400 PARMOD
10500 PARMOD1
10600 POTZ
10700 PRECNF
10800 PROOF1
10900 PROVE
11000 PRPAR
11100 PRFPRINT
11200 PRFPR1
11300 PROOF
11400 PTRS
11500 PUNIFY
11600 QUERY
11700 REAL-LNGTH
11800 REDUCER
11900 RESOLVE
12000 RESOLVE1
12100 RESUNITP
12200 RESUNITN
12300 SET1
12400 SET2
12500 SET3
12600 SETUP
12700 SEARCH2
12800 S2
12900 SETQUERY
13000 SETQUERY1
13100 SETQUERY2
13200 SETSUP
13300 SUBS3TA
13400 SUBS3T**
13500 SUB*
13600 SUBSKOL
13700 SUPPORT
13800 SUBSUME1
13900 SUBS2T
14000 SUBS3T
14100 SUBSUME
14200 SUBST1
14300 TCOPY
14400 TERMS
14500 TERMS1
14600 TERMS2
14700 TIMEIT
15000 TRY
15100 TRY1
15200 TRYIT
15300 TRAVERSE
15400 UNIT
15500 UNITS
15600 UNITRES
15700 UNITREDUCT
15800 UNITPN
15900 UNIFY
16000 UNI
16100 UNION
16200 UNWIND
16300 UPDATE
16400 UPGETL
16500 UPGETL1
16600 UPDATESTATE
16700 UPIT
16800 UPIT1
16900 UP1A
17000 UP1B
17200 VINE
17300 <)
17400 VALUE)
17500
17600 (DEFPROP ALLPOS
17700 (LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
17800 MACRO)
17900
18000 (DEFPROP ALLNEG
18100 (LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
18200 MACRO)
18300
18400 (DEFPROP ANCESTOR
18500 (LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
18600 MACRO)
18700
18800 (DEFPROP SEARCH1
18900 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
19000 MACRO)
19100
19200 (DEFPROP CONST
19300 (LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
19400 MACRO)
19500
19600 (DEFPROP HERE
19700 (LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
19800 MACRO)
19900
20000 (DEFPROP VAR
20100 (LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
20200 MACRO)
20300
22000 (DEFPROP MKWRD
22100 (LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
22200 MACRO)
22300
22400 (DEFPROP NEG
22500 (LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
22600 MACRO)
22700
22800 (DEFPROP NEGBIT
22900 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
23000 MACRO)
23100
23200 (DEFPROP POS
23300 (LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
23400 MACRO)
23500
23600 (DEFPROP POSBIT
23700 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
23800 MACRO)
23900
24000 (DEFPROP SEARCH
24100 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
24200 MACRO)
24300
24400 (DEFPROP NUM
24500 (LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
24600 MACRO)
24700
24800 (DEFPROP NEGL
24900 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
25000 MACRO)
25100
25200 (DEFPROP APPENDIT
25300 (LAMBDA(X Y)
25400 (PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
25500 EXPR)
25600
25700 (DEFPROP ANDOR
25800 (LAMBDA(C UNL EXL PF)
25900 (PROG (Z1 Z2)
26000 (SETQ Z1 (CADR C))
26100 (SETQ Z2 (CADDR C))
26200 (COND
26300 ((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
26400 (RETURN (LIST (QUOTE AND) Z1 Z2)))
26500 ((EQ (CAR Z1) (QUOTE AND))
26600 (RETURN
26700 (LIST (QUOTE AND)
26800 (CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
26900 (CNF1 (LIST (QUOTE OR) (CADDR Z1) (COPY Z2)) UNL EXL T))))
27000 ((EQ (CAR Z2) (QUOTE AND))
27100 (RETURN
27200 (LIST (QUOTE AND)
27300 (CNF1 (LIST (QUOTE OR) (CADR Z2) (COPY Z1)) UNL EXL T)
27400 (CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
27500 (T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
27600 EXPR)
27700
27800 (DEFPROP ASSOC1
27900 (LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
28000 EXPR)
28100
28200 (DEFPROP ATTEMPT
28300 (LAMBDA(Z S C)
28400 (PROG (NEWNAME SUPPORT
28500 EDITSTRAT
28600 LCL
28700 LVL
28800 CNT
28900 LSTCLS
29000 LLST
29100 Z1
29200 MERGE
29300 ORDER
29400 DEBUG
29500 DEPTH
29600 LENGTH
29700 ANCESTRY
29800 STRATEGY
29900 STRAT
30000 PMODEL
30100 NMODEL
30200 PFLG
30300 PDEPTH
30400 DLIST
30500 XYZ
30600 XYZ1
30700 COND
30800 UNAXP
30900 UNAXN
31000 SAT
31100 EE
31200 EE1
31300 CLAUSES
31400 SUBCLAUSES
31500 COUNT)
31600 (SETQ TBL (SET1 (APPEND PREFN INFN)))
31700 (SET3 Z)
31800 (SETQ Z (MINIMIZE Z))
31900 (SETQ NEWNAME (INITIAL Z))
32000 (SETQ CLAUSES Z)
32100 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
32200 (SETQ COND C)
32300 (SETQ LVL 1)
32400 (SETQ COUNT 0)
32500 (SETQ Z (UNITPN Z))
32600 (SETQ UNAXP (CAR Z))
32700 (SETQ UNAXN (CDR Z))
32800 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
32900 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
33000 (T (SETQ SUBCLAUSES CLAUSES)))
33100 (SETQ LCL (LAST CLAUSES))
33200 (SETQ LSTCLS LCL)
33300 (SETQ XYZ (SETQ EE CLAUSES))
33400 (SETQ EE1 (LAST CLAUSES))
33500 BB (SETQ LLST (CONS (CAR XYZ) LLST))
33600 (SETQ XYZ (CDR XYZ))
33700 (COND (XYZ (GO BB)))
33800 (SETQ Z1 (ERRSET (TRYIT)))
33900 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
34000 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
34100 (EVAL
34200 (LIST (QUOTE OUTC)
34300 (LIST (QUOTE OUTPUT)
34400 (QUOTE PRF)
34500 (QUOTE DSK:)
34600 (CONS (READLIST
34700 (CONS (QUOTE N)
34800 (CONS (SETQ PRNO (ADD1 PRNO))
34900 FILENAM)))
35000 (QUOTE PRF)))
35100 NIL)))
35200 (QUERY)
35300 (PROOF LHP RHP)
35400 (OUTC Z T)
35500 (RETURN Z1))
35600 (T (RETURN Z1)))))
35700 EXPR)
35800
35900 (DEFPROP AUTO
36000 (LAMBDA(X1)
36100 (PROG ( N DLIST Z2 D M SAVEED SAVESTR)
36400 (SETQ N 1)
36500 (SETQ M (SETQ D 0))
36600 A (SETQ M (MAX M (LENGTH (CDAR X1))))
36700 (SETQ D (MAX D (DEPTH (CDAR X1))))
36800 (SETQ Z2 (CAR X1))
36900 (COND
37000 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
37100 (SETQ DLIST(CONS N DLIST))))
37200 (SETQ X1 (CDR X1))
37250 (COND((NULL X1)(GO B)))
37300 (COND ((CDR X1)(SETQ N(ADD1 N)) (GO A)))
37500 (SETQ M (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2))
37600 B (COND ((NOT (GREATERP M 0)) (SETQ M 1)))
37650 (SETQ Z2(ASSOC THEOREMNAME NEWNAME))
37700 (SETQ D(ADD1 D))
37750 (COND(STRAT(COND((ZEROP ITER)(SETQ ITER 1)(COND((NOT(EQ M 1))(SETQ M(ADD1 M)))(T(SETQ D(ADD1 D)
37775 ))))(T(SETQ D(ADD1 D))(SETQ ITER 0)))))
37800 (COND(Z2
37900
38000 (SETQ SAVESTR (LIST @AND @ANCESTRY (LIST @SUPPORT THEOREMNAME))))
38100 (T (SETQ SAVESTR (QUOTE ANCESTRY))))
38200 (SETQ SAVEED
38300 (LIST @OR (LIST @MAXDEPTH @(CDR C) D)
38400 (LIST @MAXLENGTH @C M)))
38500 (COND((AND EQUAL DLIST)(SETQ SAVEED(LIST @AND (LIST @DEMOD DLIST 4) SAVEED))))
38600 (SETQ DEBUG T)
38700 (COND
38800 (EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE EQUALITY) EQUAL 3)))))))
38900 (RETURN
39000 (CONS SAVESTR SAVEED))
39100 ))
39200 EXPR)
39300
39400 (DEFPROP AUTO
39500 (NIL . T)
39600 VALUE)
39700
39800 (DEFPROP BAKSUB
39900 (LAMBDA(Z R)
40000 (PROG ( U1 U4)
40200 ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
40300 (SETQ U1 R)
40400 ED3 (SETQ U4 (CAR Z))
40500 ED1 (COND ((SUBSUME (CAR U1) U4)(DEL U4) (GO ED4)))
40600 ED6 (SETQ U1 (CDR U1))
40700 (COND (U1 (GO ED1)))
40800 ED6A (SETQ Z (CDR Z))
40900 (GO ED4)
41100 ))
41200 EXPR)
41300
41400 (DEFPROP BOOKEEP
41500 (LAMBDA(L M N)
41600 (PROG (U)
41700 B1 (SETQ U M)
41800 B3 (RPLACD (CDAAR U) (CONS 0 N))
41900 (SETQ U (CDR U))
42000 (COND ((NULL U) (RETURN (NCONC L M))))
42100 (GO B3)))
42200 EXPR)
42300
42400 (DEFPROP BUILTED
42500 (LAMBDA (X) (LIST (QUOTE LAMBDA) (QUOTE (C)) (BUILTED1 X)))
42600 EXPR)
42700
42800 (DEFPROP BUILTED1
42900 (LAMBDA(X)
43000 (COND ((ATOM X) X)
43100 ((ATOM (CAR X))
43200 (COND ((EQ (CAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDR X)) (SETQ DLIST (*CL (CADR X)CLAUSES)) NIL)
43300 (T (CONS (CAR X) (BUILTED1 (CDR X))))))
43400 ((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X)CLAUSES)) (BUILTED1 (CDR X)))
43500 (T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
43600 EXPR)
43700
43800 (DEFPROP BUILTCH
43900 (LAMBDA(X)
44000 (PROG (Z)
44050 (SETQ PFLG T)(SETQ ANCESTRY NIL)
44100 (SETQ Z (BUILTCH1 X))
44200 (RETURN
44300 (COND ((OR (ATOM Z) (EQUAL Z (QUOTE (AND))) (EQUAL X (QUOTE (OR)))) NIL)
44400 (T (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) Z))))))
44500 EXPR)
44600
44700 (DEFPROP BUILTCH1
44800 (LAMBDA(X)
44900 (COND ((ATOM X)
45000 (COND ((EQ X (QUOTE ANCESTRY)) (SETQ ANCESTRY T) NIL)
45100 ((EQ X (QUOTE NONE)) NIL)
45200 ((MEMQ X (QUOTE (VINE ALLPOS ALLNEG UNIT)))
45300 (LIST (QUOTE OR) (LIST X (QUOTE C1)) (LIST X (QUOTE C2))))
45400 (T X)))
45500 ((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE(OR (SUPPORT C2)(SUPPORT C1))))
45600 ((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
45700 (SETQ NMODEL (CADDR X))
45800 (QUOTE (OR (NOT (MODEL C1)) (NOT (MODEL C2)))))
45900 ((EQ (CAR X) (QUOTE DEFMODEL))
46000 (LIST (QUOTE OR)
46100 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C1)))
46200 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C2)))))
46300 ((EQ (CAR X) (QUOTE ANCESTRY)) (SETQ ANCESTRY T) (BUILTCH1 (CDR X)))
46400 ((ATOM (CAR X)) (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))
46500 ((EQ (CAAR X) (QUOTE EQUALITY)) (SETQ PFLG NIL)
46600 (SETQ EQUAL (CADAR X))
46700 (SETQ PDEPTH (CADDAR X))
46800 (BUILTCH1 (CDR X)))
46900 (T (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))))
47000 EXPR)
47100
47200 (DEFPROP CHOICE
47300 (LAMBDA(X)
47400 (PROG (Z Z1 Z2)
47500 (COND ((NOT (HERE X)) (RETURN NIL)) (ANCESTRY (SETQ Z (CHOICE1 X LLST))) (T (SETQ Z CLAUSES)))
47600 A (SETQ Z1 (CAR Z))
47700 (COND
47800 ((OR (NOT (HERE Z1))
47900 (AND PFLG (ALLPOS X) (ALLPOS Z1))
48000 (AND (ALLNEG Z1) (ALLNEG X))
48100 (AND STRATEGY (NOT (STRATEGY X Z1))))
48200 NIL)
48300 (T (SETQ Z2 (NCONC Z2 (LIST Z1)))))
48400 (SETQ Z (CDR Z))
48500 (COND ((OR (EQ Z X) (NULL Z)) (RETURN Z2)))
48600 (GO A)))
48700 EXPR)
48800
48900 (DEFPROP CHOICE1
49000 (LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
49100 EXPR)
49200
49300 (DEFPROP CLAUSES
49400 (LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
49500 EXPR)
49600
49700 (DEFPROP CLAUSES2
49800 (LAMBDA (U) (CLAUSES1 U CNT))
49900 EXPR)
50000
50100 (DEFPROP CLAUSES1
50200 (LAMBDA(U N)
50300 (PROG NIL
50400 (COND ((NOT DEBUG) (RETURN NIL)))
50500 (COND ((NULL (CAR U)) (RETURN NIL)))
50600 CL1 (COND ((NULL U) (RETURN NIL)))
50700 (UP1A (CAR U) N)
50800 CL2 (SETQ U (CDR U))
50900 (SETQ N (ADD1 N))
51000 (GO CL1)))
51100 EXPR)
51200
51300 (DEFPROP CNF
51400 (LAMBDA(C1)
51500 (PROG (C)
51600 (SETQ C (PRECNF C1))
51700 (RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
51800 EXPR)
51900
52000 (DEFPROP CNF1
52100 (LAMBDA(C UNL EXL PF)
52200 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
52300 ((MEMQ (CAR C) (QUOTE (AND OR)))
52400 (ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
52500 ((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
52600 (CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
52700 ((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
52800 (CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
52900 (PF (SUBSKOL C EXL))
53000 (T (CONS ESCAPE (SUBSKOL C EXL)))))
53100 EXPR)
53200
53300 (DEFPROP CNF2
53400 (LAMBDA(C)
53500 (COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
53600 ((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
53700 (T (LIST (LIST C)))))
53800 EXPR)
53900
54000 (DEFPROP CNF3
54100 (LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
54200 EXPR)
54300
54400 (DEFPROP CNVT
54500 (LAMBDA(Z)
54600 (PROG (ZP ZN VARL VARNO)
54700 (SETQ VARNO 0)
54800 (COND
54900 ((EQ (LENGTH Z) 1)
55000 (RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
55100 A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
55200 (SETQ ZP (CNVT2 (CAR Z)))
55300 AP1 (SETQ Z (CDR Z))
55400 (COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
55500 (SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
55600 (GO AP1)
55700 AN1 (SETQ ZN (CNVT2 (CDAR Z)))
55800 AN1B (SETQ Z (CDR Z))
55900 AN1A (COND ((NULL Z) (GO AN2)))
56000 (SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
56100 (GO AN1B)
56200 AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
56300 ((NULL ZN) (RETURN ZP))
56400 (T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
56500 EXPR)
56600
56700 (DEFPROP CNVT2
56800 (LAMBDA(X)
56900 (COND ((ATOM X) X)
57000 ((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
57100 ((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
57200 (T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
57300 EXPR)
57400
57500 (DEFPROP CNVT3
57600 (LAMBDA(X)
57700 (PROG (Z)
57800 (SETQ Z (ASSOC X VARL))
57900 (COND (Z (RETURN (CDR Z))))
58000 (SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
58100 (RETURN VARNO)))
58200 EXPR)
58300
58400 (DEFPROP COPY
58500 (LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
58600 EXPR)
58700
58800 (DEFPROP COPYDELETED
58900 (LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
59000 EXPR)
59100
59200 (DEFPROP *CL
59300 (LAMBDA (C X) (UPGETL1 C X (CONS (CONS (QUOTE CLAUSES) X) NEWNAME)))
59400 EXPR)
59500
59600 (DEFPROP DEMOD
59700 (LAMBDA(X L)
59800 (PROG (S1 S2)
59900 (SETQ S1 (CDAR X))
60000 A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
60100 (T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
60200 (COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
60300 (SETQ S1 (CDR S1))
60400 (COND (S1 (GO A)))
60500 (RETURN X)
60600 ))
60700 EXPR)
60800
60900 (DEFPROP DEM
61000 (LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
61100 EXPR)
61200
61300 (DEFPROP DEPTH
61400 (LAMBDA(Z)
61500 (PROG (Z1 Z2)
61600 (SETQ Z1 0)
61700 D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
61800 (SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
61900 (SETQ Z (CDR Z))
62000 (COND (Z (GO D1)))
62100 (RETURN Z1)))
62200 EXPR)
62300
62400 (DEFPROP DEPTH
62500 (NIL . 10)
62600 VALUE)
62700
62800 (DEFPROP DEPTH1
62900 (LAMBDA(Z)
63000 (PROG (Z1)
63100 (SETQ Z1 0)
63200 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
63300 (SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
63400 D2 (SETQ Z (CDR Z))
63500 (COND (Z (GO D1)))
63600 (RETURN Z1)))
63700 EXPR)
63800
63900 (DEFPROP DEL
64000 (LAMBDA (C) (RPLACA (CAR C) NIL))
64100 EXPR)
64200
65000
65100 (DEFPROP DOWN
65200 (LAMBDA(N L)
65300 (PROG NIL
65400 (COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
65500 D1 (SETQ N (SUB1 N))
65600 (COND ((ZEROP N) (RETURN L)))
65700 (SETQ L (CDR L))
65800 (COND (L (GO D1)))
65900 (RETURN NIL)))
66000 EXPR)
66100
66200 (DEFPROP EDIT
66300 (LAMBDA(U Z)
66400 (PROG (RES1 U1 U4)
66500 ED4 (COND ((NULL Z) (RETURN RES1)))
66600 (SETQ U4 (CAR Z))
66700 (COND ((EDITSTRAT U4) (GO ED2)))
66800 (SETQ U1 SUBCLAUSES)
66900 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
67000 ED6 (SETQ U1 (CDR U1))
67100 (COND (U1 (GO ED1)))
67200 (SETQ U1 (CDR Z))
67300 (COND ((NULL U1) (GO ED5)))
67400 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
67500 ED7 (SETQ U1 (CDR U1))
67600 (COND (U1 (GO ED3)))
67700 ED5 (SETQ RES1 (CONS U4 RES1))
67800 ED2 (SETQ Z (CDR Z))
67900 (GO ED4)))
68000 EXPR)
68100
68200 (DEFPROP ERPRINT
68300 (LAMBDA (X) (COND (DEBUG (PRINT X))))
68400 EXPR)
68500
68600 (DEFPROP ERPRIN1
68700 (LAMBDA (X) (COND (DEBUG (PRIN1 X))))
68800 EXPR)
68900
69000 (DEFPROP EXPUNGE
69100 (LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
69200 EXPR)
69300
69400 (DEFPROP FINI
69500 (LAMBDA(U R Z1 Z2 E)
69600 (PROG (Z)
69700 (COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
69800 (COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
69900 (SETQ COUNT (PLUS COUNT (LENGTH R)))
70000 (SETQ R (EDIT U R))
70100 (CLAUSES2 R)
70200 (COND ((NULL R) (RETURN 0)))
70300 (BAKSUB CLAUSES R)
70400 (BOOKEEP E R (CONS Z1 Z2))
70500 (SETQ Z (UNITPN R))
70600 (SETQ UNAXP (APPEND (CAR Z) UNAXP))
70700 (SETQ UNAXN (APPEND (CDR Z) UNAXN))
70800 (RETURN (LENGTH R))))
70900 EXPR)
71000
71100 (DEFPROP FIXNEG
71200 (LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
71300 EXPR)
71400
71500 (DEFPROP FIXQFF
71600 (LAMBDA(C)
71700 (PROG (Z)
71800 (SETQ Z (FIXQFF1 C NIL NIL NIL))
71900 (COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
72000 EXPR)
72100
72200 (DEFPROP FIXQFF1
72300 (LAMBDA(C NEW FA TE)
72400 (PROG (Z)
72500 (COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
72600 ((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
72700 ((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
72800 ((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
72900 ((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
73000 (RETURN
73100 (FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
73200 (SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
73300 A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
73400 ((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
73500 (SETQ NEW (CONS (CAR Z) NEW))
73600 B (SETQ Z (CDR Z))
73700 (GO A)))
73800 EXPR)
73900
74000 (DEFPROP GENSKOLEM
74100 (LAMBDA(VARL UNL)
74200 (PROG (Z)
74300 A (COND ((NULL VARL) (RETURN Z)))
74400 (SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
74500 (SETQ VARL (CDR VARL))
74600 (GO A)))
74700 EXPR)
74800
74900 (DEFPROP GETNAME
75000 (LAMBDA(X L)
75100 (PROG (Z)
75200 (SETQ Z (ASSOC X L))
75300 (COND (Z (RETURN (CDR Z))))
75400 (PRINT X)
75500 (PRINC (QUOTE IS-AN-UNBOUND-NAME))
75600 (RETURN NIL)))
75700 EXPR)
75800
75900 (DEFPROP GETTERMS
76000 (LAMBDA (E NAMELIST)
76100 (PROG (Z )
76200 (SCANSET)
76300 (START)
76400 (SETQ Z (ERRSET (<TM>) T))
76500 (SCANRESET)
76600 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
76700 (SETQ XYZ (TOP))
76800 (COND ((NOT (EQ (READ) (QUOTE FOR))) (RETURN NIL)))
76900 (SCANSET)
77000 (START)
77100 (SETQ Z (ERRSET (<TM>) T))
77200 (SCANRESET)
77300 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
77400 (SETQ XYZ1 (TOP))
77500 (COND ((NOT (EQ (READ) (QUOTE IN))) (RETURN NIL)))
77600 (RETURN (UPGETL E NAMELIST))))
77700 EXPR)
77800
77900 (DEFPROP GETVARS
78000 (LAMBDA(C)
78100 (PROG (Z)
78200 A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
78300 ((CONST (CAR C)) NIL)
78400 (T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
78500 (SETQ C (CDR C))
78600 (COND (C (GO A)))
78700 (RETURN Z)))
78800 EXPR)
78900
79000 (DEFPROP GOLIST
79100 (NIL (EO . UEO1)
79200 (DS . UDS1)
79300 (CH . UCH1)
79400 (SY . USY1)
79500 (CU . UCU1)
79600 (FL . UFL1)
79700 (DI . UDI1)
79800 (ST . UST1)
79900 (HA . UST1)
80000 (DE . UDE1)
80100 (IN . UIN1)
80200 (EV . UEV1)
80300 (QU . UQU1)
80400 (TR . UTR1)
80500 (UP . UUP1)
80600 (ME . UME1)
80700 (SI . USI1)
80800 (SE . USE1)
80900 (DO . UDO1)
81000 (CL . UCL1)
81100 (SU . USU1)
81200 (AN . UAN1)
81300 (TE . UTE1)
81400 (RE . URE1)
81500 (SA . USA1)
81600 (PA . UPA1)
81700 (ED . UED1)
81800 (US . UUS1)
81900 (PR . UPR1)
82000 (FU . UFL2)
82100 (FD . UFL3)
82200 (GO . UGO1)
82300 (EX . UEX1)
82400 (AB . UAB1)
82500 (HE . UHE1))
82600 VALUE)
82700
82800 (DEFPROP INCLAUSES
82900 (LAMBDA NIL
83000 (PROG (Z Z1 AXNO)
83100 (SETQ AXNO (QUOTE AXIOM))
83200 A (SCANSET)
83300 (START)
83400 (SETQ ZIN (ERRSET (<INPUT>) T))
83500 (SCANRESET)
83600 (COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
83700 (SETQ ZIN (TOP))
83800 (COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
83900 ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
84000 ((MEMQ (CAR ZIN) DECOP) (GO B)))
84100 (OUT >S< ZIN)
84200 (SETQ Z
84300 (APPEND Z
84400 (SETUP
84500 (CNF (COND ((EQ AXNO THEOREMNAME) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
84600 (GO A)
84700 B (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
84800 (COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (APPEND IVAR (CDR ZIN)))))
84900 ((EQ Z1 (QUOTE EQUAL)) (SETQ PFLG NIL) (SETQ EQUAL (CADR ZIN)))
85000 (T (SET Z1 (APPEND (CDR ZIN) (EVAL Z1)))))
85100 (OUT >INPUT< ZIN)
85200 (GO A)))
85300 EXPR)
85400
85500 (DEFPROP INITIAL
85600 (LAMBDA(L)
85700 (PROG (ST Z Z1 Z2)
85800 A (SETQ Z (CDR (ANCESTOR (CAR L))))
85900 (COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
86000 ((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
86100 (T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
86200 (SETQ Z2 (CONS (CAR L) Z2))
86300 (SETQ L (CDR L))
86400 (COND (L (GO A)))
86500 (RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
86600 EXPR)
86700
86800 (DEFPROP INITIALAX
86900 (LAMBDA(L)
87000 (PROG (Z Z1 Z2 Z3 AXNO)
87100 (SETQ AXNO (CAR L))
87200 (SETQ L (CDR L))
87300 A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
87400 (SETQ Z1 (ANCESTOR (CAR L)))
87500 (COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
87600 (SETQ Z2 (ANCESTOR Z))
87700 (RPLACA Z2 Z1)
87800 (RPLACD Z2 AXNO)
87900 (SETQ Z3 (CONS Z Z3))
88000 B (SETQ L (CDR L))
88100 (COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
88200 (GO A)))
88300 EXPR)
88400
88500 (DEFPROP INITIALAX1
88600 (LAMBDA(L1)
88700 (PROG (Z L2 L)
88800 (SETQ L L1)
88900 B1 (SETQ L2 L)
89000 A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
89100 (SETQ L2 (CDR L2))
89200 (COND (L2 (GO A1)))
89300 (SETQ L (CDR L))
89400 (COND (L (GO B1)))
89500 (SETQ L L1)
89600 B (SETQ Z (CDDAAR L))
89700 (COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
89800 ((NUMBERP (CAAAR L)) NIL)
89900 (T (RPLACA (CAAR L) (CAAAAR L))))
90000 (COND ((ATOM (CDDR Z)) (GO A)))
90100 (RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
90200 A (SETQ L (CDR L))
90300 (COND (L (GO B)))
90400 (RETURN L1)))
90500 EXPR)
90600
90700 (DEFPROP MAKVAR
90800 (LAMBDA(X)
90900 (CDR(ASSOC X VARTBL)))EXPR)
91500
91600 (DEFPROP MAKOVAR
91700 (LAMBDA(X)
91800 (PROG (X1 *NOPOINT Z Z1 M)
91900 (SETQ *NOPOINT T)
92200 (SETQ X1 X)
92300 D(SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO(CAR X1)))))
92350 (SETQ VARTBL(NCONC VARTBL(LIST(CONS (CAR X1)VARNO))))
92400 (SETQ X1 (CDR X1))
92500 (SETQ VARNO(ADD1 VARNO))
92600 (COND (X1 (GO D)))
92700 B (SETQ Z (EXPLODE (CAR X)))
92800 (COND ((NUMBERP (CAR (LAST Z))) (GO A)))
92900 (SETQ M 1)
92950 C(SETQ Z1(READLIST(APPEND Z(LIST M))))
92975 (SETQ IVAR(CONS Z1 IVAR))
93000 (SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO Z1))) )
93050 (SETQ VARTBL(NCONC VARTBL(LIST(CONS Z1 VARNO))))
93100 (COND ((LESSP M 11) (SETQ VARNO(ADD1 VARNO)) (SETQ M (ADD1 M)) (GO C)))
93200 A (SETQ X (CDR X))
93300 (COND (X (SETQ VARNO (ADD1 VARNO)) (GO B)))
93500 (RETURN OUTVAR)))
93600 EXPR)
93700
93800 (DEFPROP MAPIT
93900 (LAMBDA(X XYZ N)
94000 (PROG (Z Z1 Z2)
94100 (SETQ Z (GETNAME X N))
94200 (COND ((NULL Z) (RETURN NIL)))
94300 A (SETQ ZIN (CAR Z))
94400 (SETQ Z2 (ERRSET (XYZ ZIN) T))
94500 (COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
94600 ((NULL (CAR Z2)) NIL)
94700 (T (SETQ Z1 (CONS (CAR Z) Z1))))
94800 (SETQ Z (CDR Z))
94900 (COND (Z (GO A)))
95000 (RETURN (REVERSE Z1))))
95100 EXPR)
95200
05800
05900 (DEFPROP MAX
06000 (LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
06100 EXPR)
06200
06300 (DEFPROP MEMC
06400 (LAMBDA(C L)
06500 (PROG NIL
06600 (COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
06700 B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
06800 (SETQ L (CDR L))
06900 (COND (L (GO B)))
07000 (RETURN NIL)
07100 A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
07200 (SETQ L (CDR L))
07300 (COND (L (GO A)))
07400 (RETURN NIL)))
07500 EXPR)
07600
07700 (DEFPROP MIN1
07800 (LAMBDA(L)
07900 (PROG (Z Z1)
08000 (SETQ Z (CAR L))
08100 M1 (SETQ Z1 (CDR L))
08200 (COND ((NULL Z1)
08300 (COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
08400 ((NUMBERP (CAAR Z1)) (GO M2))
08500 ((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
08600 M2 (SETQ L (CDR L))
08700 (GO M1)))
08800 EXPR)
08900
09000 (DEFPROP MINIMIZE
09100 (LAMBDA(Z3)
09200 (PROG (Z1 Z2 Z4)
09300 (SETQ Z2 (LIST (CAR Z3)))
09400 ED2 (SETQ Z3 (CDR Z3))
09500 (COND ((NULL Z3) (RETURN (REVERSE Z2))))
09600 (SETQ Z4 (CAR Z3))
09700 (SETQ Z1 Z2)
09800 ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
09900 (SETQ Z1 (CDR Z1))
10000 (COND (Z1 (GO ED1)))
10100 (SETQ Z1 (CDR Z3))
10200 ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
10300 (SETQ Z1 (CDR Z1))
10400 (GO ED4)
10500 ED5 (SETQ Z2 (CONS Z4 Z2))
10600 (GO ED2)))
10700 EXPR)
10800
10900 (DEFPROP MIN
11000 (LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
11100 EXPR)
11200
11300 (DEFPROP MKSYM
11400 (LAMBDA NIL
11500 (PROG NIL
11600 (SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
11700 (SETQ PREFN (CONS (CAR FNLIST) PREFN))
11800 (RETURN (CAR FNLIST))))
11900 EXPR)
12000
12100 (DEFPROP MODEL
12200 (LAMBDA(C)
12300 (PROG (Z)
12400 (SETQ Z (CDR C))
12500 M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
12600 M2 (SETQ Z (CDR Z))
12700 (COND (Z (GO M1)))
12800 (RETURN NIL)
12900 M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
13000 (GO M2)))
13100 EXPR)
13200
13300 (DEFPROP NCONC1
13400 (LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
13500 EXPR)
13600
13700 (DEFPROP NEGATE
13800 (LAMBDA(Z)
13900 (PROG (BDY)
14000 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
14100 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
14200 (SETQ Z (CDDR Z))
14300 C (COND ((NULL Z) (GO D)))
14400 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
14500 (SETQ Z (CDR Z))
14600 (GO C)
14700 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
14800 EXPR)
14900
15000 (DEFPROP NEGSGN
15100 (NIL . ¬)
15200 VALUE)
15300
17100
17200 (DEFPROP ONEGSGN
17300 (NIL . ¬)
17400 VALUE)
17500
17600 (DEFPROP *NOPOINT
17700 (NIL . T)
17800 VALUE)
17900
18000 (DEFPROP OCCUR
18100 (LAMBDA(X Z)
18200 (PROG (Z1)
18300 OC1 (SETQ Z1 (CAR Z))
18400 (COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
18500 ((CONST Z1) (GO OC2))
18600 ((OCCUR X (CDR Z1)) (RETURN T)))
18700 OC2 (SETQ Z (CDR Z))
18800 (COND (Z (GO OC1)))
18900 (RETURN NIL)))
19000 EXPR)
19100
19200 (DEFPROP ORDER
19300 (LAMBDA(X Y)
19400 (COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
19500 ((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
19600 EXPR)
19700
19800 (DEFPROP ORDEREQUAL
19900 (LAMBDA(S)
20000 (PROG NIL
20100 (COND ((VAR (CAR S))
20200 (COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
20300 ((CONST (CAR S))
20400 (COND ((VAR (CADR S)) (RETURN NIL))
20500 ((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
20600 (T (GO A))))
20700 ((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
20800 ((MAXDEPTH1(CDAR S)(DEPTH1(CDADR S)))(RETURN NIL)))
20900 A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
21000 EXPR)
21100
21200 (DE ORDEREQUAL1(X)(PROG(S1 S2)
21300 (SETQ S1(CDAR X))B(SETQ S2(COND((NEG(CAR S1))(CDAR S1))(T(CAR S1))))
21400 (COND((EQ(CAR S2 )EQUAL)(ORDEREQUAL (CDR S2))))
21500 (SETQ S1(CDR S1))(COND(S1(GO B)))(RETURN X)))
21600
21700 (DEFPROP PARMOD
21800 (LAMBDA(C D)
21900 (COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
22000 EXPR)
22100
22200 (DEFPROP PARMOD1
22300 (LAMBDA(C D)
22400 (PROG (PF YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
22500 (SETQ YC (CDR C))
22600 PAR1 (SETQ YD (CDR D))
22700 (SETQ X (CAR YC))
22800 (COND ((NEG X) (RETURN PAR))
22900 ((ORDERP (CAR X) EQUAL) (GO PAR2))
23000 ((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
23100 PAR3 PAR3A
23200 (COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
23300 (SETQ Y1 (CDDR X))
23400 (SETQ Y2 (CADR X))
23500 PAR3B
23600 (COND ((VAR (CAR Y1)) (GO PAR7A)))
23700 (SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
23800 (COND ((NULL Z) (GO PAR7A)))
23900 PAR5 (SETQ Z1 Z)
24000 PAR4 (COND
24100 ((CONST (CAR Y1))
24200 (COND ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7))
24300 (T (SETQ TS (COPY Y2)) (GO PAR9))))
24400 ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7)))
24500 (SETQ Y (UNIFY (CDAR Y1) (CDAAR Z1)))
24600 (COND (Y (SETQ Y (CDR Y)) (GO PAR6)))
24700 PAR7 (SETQ Z1 (CDR Z1))
24800 (COND (Z1 (GO PAR4)))
24900 PAR7A
25000 (COND ((NULL PF) (SETQ PF T) (SETQ Y1 (LIST Y2)) (SETQ Y2 (CADDR X)) (GO PAR3B)))
25100 PAR7B
25200 (SETQ YD (CDR YD))
25300 (COND (YD (GO PAR3A)))
25400 PAR2 (SETQ YC (CDR YC))
25500 (COND (YC (GO PAR1)))
25600 (RETURN PAR)
25700 PAR6 (SETQ TS (CADR (SUBS3T* Y (LIST NIL Y2))))
25800 PAR9 (SETQ PARRES (SUBS3TA Y Z2 (CAR Z1) TS))
25900 (COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
26000 (SETQ Y (UNION Y C D X (CAR YD)))
26100 (COND ((NULL Y) (GO PAR7)))
26200 (SETQ PAR (CONS (SET2 (CAR (COND (DLIST (DEMOD Y DLIST))(EQUAL(ORDEREQUAL1 Y)) (T Y))) TBL) PAR))
26300 (GO PAR7)))
26400 EXPR)
26500
26600 (DEFPROP POTZ
26700 (LAMBDA(X)
26800 (PROG (Z Z1)
26900 (SETQ Z (POTZ1 X))
27000 (COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
27100 (SETQ POTZTBL (CONS Z POTZTBL))
27200 (RETURN Z)))
27300 EXPR)
27400
27500 (DEFPROP PRECNF
27600 (LAMBDA(X)
27700 (COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
27800 ((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
27900 ((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
28000 ((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
28100 ((EQ (CAR X) (QUOTE EQUIV))
28200 (LIST (QUOTE AND)
28300 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
28400 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
28500 (T X)))
28600 EXPR)
28700
28800 (DEFPROP PROOF1
28900 (LAMBDA(L)
29000 (PROG (Q X Y Z P P1)
29100 (PRINC (QUOTE / ))
29200 (PRINC (QUOTE / ))
29300 (PRFPRINT (CDR L))
29400 (SETQ P (ANCESTOR L))
29500 (COND ((ATOM (CDR P)) (GO P3)))
29600 (SETQ P1 (CDR P))
29700 (SETQ P (CAR P))
29800 (PRINC (QUOTE / ))
29900 (PRINC 1)
30000 (PRINC (QUOTE / ))
30100 (PRINC 2)
30200 (SETQ X 1)
30300 (SETQ Y 2)
30400 (SETQ Q (LIST (CONS X P) (CONS Y P1)))
30500 P1 (SETQ Z (ANCESTOR (CDAR Q)))
30600 (COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
30700 (SETQ X (ADD1 Y))
30800 (SETQ Y (ADD1 X))
30900 (PRINT (CAAR Q))
31000 (PRFPRINT (CDDAR Q))
31100 (PRINC X)
31200 (PRINC (QUOTE / ))
31300 (PRINC Y)
31400 (SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
31500 P2 (SETQ Q (CDR Q))
31600 (COND ((NULL Q) (RETURN NIL)))
31700 (GO P1)
31800 P3 (PRIN1 (CDR P))
31900 (RETURN (TERPRI))))
32000 EXPR)
32100
32200 (DEFPROP PROVE
32300 (LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
32400 FEXPR)
32500
32600 (DEFPROP PRPAR
32700 (LAMBDA(L)
32800 (PROG NIL
32900 (CLAUSES CLAUSES)
33000 (TERPRI)
33100 P1 (PROOF1 (CAR L))
33200 (TERPRI)
33300 (TERPRI)
33400 (SETQ L (CDR L))
33500 (COND (L (GO P1)))
33600 (RETURN NIL)))
33700 EXPR)
33800
33900 (DEFPROP PRFPRINT
34000 (LAMBDA(X)
34100 (PROG NIL
34200 (SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
34300 (SETQ LAST NIL)
34400 (FPRINT &&Z 0)))
34500 EXPR)
34600
34700 (DEFPROP PRFPR1
34800 (LAMBDA(L)
34900 (PROG (Z)
35000 (COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
35100 (PRINC (CAR L))
35200 (SETQ L (CDR L))
35300 (PRINC (QUOTE /())
35400 P1 (COND ((VAR (CAR L))
35500 (COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
35600 (T (PRINC (QUOTE X))
35700 (COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
35800 (T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
35900 ((CONST (CAR L)) (PRINC (CAAR L)))
36000 (T (PRFPR1 (CAR L))))
36100 P2 (SETQ L (CDR L))
36200 (COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
36300 (PRINC (QUOTE /,))
36400 (GO P1)))
36500 EXPR)
36600
36700 (DEFPROP PROOF
36800 (LAMBDA(L R)
36900 (PROG (Q Q1 X Z)
37000 (SETQ LHP L)
37100 (SETQ RHP R)
37200 (RPLACA (MKWRD L) 1)
37300 (RPLACA (MKWRD R) 2)
37400 (SETQ X 2)
37500 (SETQ Q (LIST L R))
37600 (SETQ Q1 Q)
37700 P1 (SETQ Z (ANCESTOR (CAR Q)))
37800 (COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
37900 (RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
38000 (RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
38100 (NCONC Q (LIST (CAR Z) (CDR Z)))
38200 P2 (SETQ Q (CDR Q))
38300 (COND (Q (GO P1)))
38400 (PRINT (QUOTE NIL))
38500 (PRINC (CAR (MKWRD (CAR Q1))))
38600 (PRINC (QUOTE / ))
38700 (PRINC (CAR (MKWRD (CADR Q1))))
38800 (SETQ X 1)
38900 A (COND
39000 ((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
39100 (PRFPRINT (CDAR Q1))
39200 (COND
39300 ((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
39400 ((ATOM (CDR (ANCESTOR (CAR Q1))))
39500 (PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
39600 (PRINC (QUOTE / ))
39700 (PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
39800 (T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
39900 (PRINC (QUOTE / ))
40000 (PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
40100 (SETQ Q1 (CDR Q1))
40200 (SETQ X (ADD1 X))
40300 (COND (Q1 (GO A)))))
40400 EXPR)
40500
40600 (DEFPROP PTRS
40700 (LAMBDA(X)
40800 (PROG (Z)
40900 A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
41000 (SETQ X (CDR X))
41100 (COND (X (GO A)))
41200 (RETURN Z)))
41300 EXPR)
41400
41500 (DEFPROP PUNIFY
41600 (LAMBDA(X Y)
41700 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
41800 (SETQ LC (LIST NIL))
41900 U3 (SETQ Z1 (CAR X))
42000 (SETQ Z2 (CAR Y))
42100 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
42200 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
42300 (COND ((VAR Z3)
42400 (COND ((VAR Z4) (GO UN1))
42500 ((CONST Z4) (GO UN3))
42600 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
42700 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
42800 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
42900 ((VAR Z4) (RETURN NIL))
43000 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
43100 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
43200 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
43300 (SETQ X (APPEND Z6 (CDR X)))
43400 (SETQ Y (APPEND Z7 (CDR Y)))
43500 (GO U3))
43600 (T (RETURN NIL)))
43700 UN1 (SUBS2T Z3 Z4 LC)
43800 UN2 (SETQ X (CDR X))
43900 (COND (X (SETQ Y (CDR Y)) (GO U3)))
44000 (RETURN LC)
44100 UN3 (SUBS2T Z4 Z3 LC)
44200 (GO UN2)))
44300 EXPR)
44400
44500 (DEFPROP QUERY
44600 (LAMBDA NIL
44700 (PROG NIL
44800 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
44900 (OUTIT(CAR STRAT))
45000 (PRINT (QUOTE EDIT-STRATEGY-IS:))
45100 (OUTIT(CDR STRAT))
45200 (PRINT (QUOTE ELAPSED-TIME))
45300 (PRINC (QUOTE =))
45400 (PRINC (TIMEIT))
45500 (RETURN (TERPRI))))
45600 EXPR)
45700
45800 (DEFPROP REAL-LNGTH
45900 (LAMBDA(L)
46000 (PROG (N)
46100 (SETQ N 0)
46200 A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
46300 (SETQ L (CDR L))
46400 (GO A)))
46500 EXPR)
46600
46650 (DE REENTER()(TRYIT))
46700 (DEFPROP REDUCER
46800 (LAMBDA(C L)
46900 (PROG (Z Z1 Z2 Z3 C1)
47000 (SETQ Z (CDAR C))
47100 (SETQ Z2 (CDAAR C))
47200 (SETQ C1 C)
47300 (SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
47400 A (COND ((EQ L (CDR C1)) (GO B)))
47500 (SETQ C1 (CDR C1))
47600 (SETQ Z1 (CDR Z1))
47700 (GO A)
47800 B (RPLACD C1 (CDDR C1))
47900 (COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
48000 (COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
48100 (RPLACD Z1 (CDDR Z1))
48200 (RPLACA Z2 (CDR Z3))
48300 (RPLACA (CAAR C) (SUB1 (CAAAR C)))
48400 (RETURN C)))
48500 EXPR)
48600
48700 (DEFPROP RESOLVE
48800 (LAMBDA(C D)
48900 (COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
49000 ((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
49100 (T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
49200 EXPR)
49300
49400 (DEFPROP RESOLVE1
49500 (LAMBDA(C D)
49600 (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
49700 (COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
49800 (SETQ YC (CDR C))
49900 (SETQ CB (POSBIT C))
50000 (SETQ YD1 (NEGL D))
50100 (SETQ DB1 (NEGBIT D))
50200 (SETQ DB DB1)
50300 (SETQ YD YD1)
50400 RES1 (SETQ X (CAR YC))
50500 (COND ((NEG X) (RETURN RES)))
50600 (SETQ Y (CAR YD))
50700 (COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
50800 (SETQ YD1 YD)
50900 (SETQ DB1 DB)
51000 (GO RES2A)
51100 RES2 (SETQ Y (CAR YD))
51200 (COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
51300 RES2A
51400 (COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
51500 (SETQ Z (UNIFY (CDR X) (CDDR Y)))
51600 (COND ((NULL Z) (GO RES2B)))
51700 (SETQ PARRES NIL)
51800 (SETQ Z (UNION (CDR Z) C D X Y))
51900 (COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
52000 (SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST))(EQUAL(ORDEREQUAL1 Z)) (T Z))) TBL) RES))
52100 RES2B
52200 (SETQ YD (CDR YD))
52300 (COND (YD (SETQ DB (CDR DB)) (GO RES2)))
52400 RES3A
52500 (SETQ DB DB1)
52600 (SETQ YD YD1)
52700 RES3 (SETQ YC (CDR YC))
52800 (COND (YC (SETQ CB (CDR CB)) (GO RES1)))
52900 (RETURN RES)
53000 RES4 (SETQ YD (CDR YD))
53100 (COND (YD (SETQ DB (CDR DB)) (GO RES1)))
53200 (GO RES3A)))
53300 EXPR)
53400
53500 (DEFPROP RESUNITP
53600 (LAMBDA(P TM L)
53700 (PROG (Z)
53800 A (SETQ Z (CDADAR L))
53900 (COND ((EQ (CAR Z) P) (GO C)))
54000 B (SETQ L (CDR L))
54100 (COND (L (GO A)))
54200 (RETURN NIL)
54300 C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
54400 (GO B)))
54500 EXPR)
54600
54700 (DEFPROP RESUNITN
54800 (LAMBDA(P TM L)
54900 (PROG (Z)
55000 A (SETQ Z (CADAR L))
55100 (COND ((EQ (CAR Z) P) (GO C)))
55200 B (SETQ L (CDR L))
55300 (COND (L (GO A)))
55400 (RETURN NIL)
55500 C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
55600 (GO B)))
55700 EXPR)
55800
55900
56000 (DEFPROP SET1
56100 (LAMBDA(L)
56200 (PROG (TBL N)
56300 (SETQ N 1)
56400 (SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
56500 A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
56600 (SETQ L (CDR L))
56700 (COND (L (SETQ N (ADD1 N)) (GO A)))
56800 (RETURN (SETU TBL))))
56900 EXPR)
57000
57100 (DEFPROP SET2
57200 (LAMBDA(C L)
57300 (PROG (X Z T1 T2 T3* T2* T3 Z1)
57400 (SETQ T2 (SETQ T2* (LIST NIL)))
57500 (SETQ T3 (SETQ T3* (LIST NIL)))
57600 (SETQ X (CDR C))
57700 S1 (SETQ Z (CDAR X))
57800 (SETQ T1 NIL)
57900 (COND ((NEG (CAR X)) (GO S2)))
58000 S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
58100 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
58200 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
58300 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
58400 (SETQ Z (CDR Z))
58500 (COND (Z (GO S1A)))
58600 (SETQ X (CDR X))
58700 (RPLACD T2* (LIST (POTZ T1)))
58800 (SETQ T2* (CDR T2*))
58900 (COND (X (GO S1)))
59000 S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
59100 (RPLACA (CAR C) (CONS (CAAR C) T3))
59200 (RETURN C)
59300 S2 (SETQ Z (CDDAR X))
59400 (SETQ T1 NIL)
59500 S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
59600 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
59700 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
59800 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
59900 (SETQ Z (CDR Z))
60000 (COND (Z (GO S2A)))
60100 (SETQ X (CDR X))
60200 (RPLACD T3* (LIST (POTZ T1)))
60300 (SETQ T3* (CDR T3*))
60400 (COND (X (GO S2)))
60500 (GO S4)))
60600 EXPR)
60700
60800 (DEFPROP SET3
60900 (LAMBDA(Z)
61000 (PROG (E)
61100 (COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
61200 (SETQ E Z)
61300 S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
61400 (SETQ E (CDR E))
61500 (COND (E (GO S1)))
61600 (RETURN Z)))
61700 EXPR)
61800
61900 (DEFPROP SETUP
62000 (LAMBDA(Z)
62100 (PROG (BL Z1 Z2 Z3 Z4 Z5)
62200 SET2 (SETQ Z3 (CAR Z))
62300 (SETQ Z2 0)
62400 (SETQ BL NIL)
62500 (SETQ NO* NO)
62600 (SETQ Z5 NIL)
62700 S1 (SETQ Z4 (MIN1 Z3))
62800 (COND ((NULL Z4) (GO S3)))
62900 (UPIT Z4)
63000 (COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
63100 (SETQ Z2 (ADD1 Z2))
63200 (SETQ Z5 (CONS Z4 Z5))
63300 (GO S1)
63400 S3 (SETQ Z3 NIL)
63500 (SETQ Z4 Z5)
63600 S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
63700 (SETQ Z4 (CDR Z4))
63800 (COND (Z4 (GO S2)))
63900 SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
64000 SET1 (SETQ Z1 (CONS Z5 Z1))
64100 S4 (SETQ Z (CDR Z))
64200 (COND (Z (GO SET2)))
64300 (RETURN Z1)))
64400 EXPR)
64500
64600 (DEFPROP SEARCH2
64700 (LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
64800 EXPR)
64900
65000 (DEFPROP S2
65100 (LAMBDA(X Y Z)
65200 (PROG (Z1)
65300 (SETQ Z1 (CDR Z))
65400 A (COND ((NULL Z1) (RETURN Z))
65500 ((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
65600 ((CONST (CAR Z1)) NIL)
65700 (T (RPLACA Z1 (S2 X Y (CAR Z1)))))
65800 (SETQ Z1 (CDR Z1))
65900 (GO A)))
66000 EXPR)
66100
66200 (DEFPROP SETQUERY
66300 (LAMBDA (X) (SETQUERY2 X NIL NIL))
66400 EXPR)
66500
66600 (DEFPROP SETQUERY1
66700 (LAMBDA(XYZ XYZ1)
66800 (PROG (Z)
66900 (SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
67000 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
67100 (RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
67200 EXPR)
67300
67400 (DEFPROP SETQUERY2
67500 (LAMBDA(XX YY FLG)
67600 (PROG (XYZ1 CHAN
67700 Z
67800 Z1
67900 SAVESTR SAVEED)
68000 (SETQ CHAN (OUTC NIL NIL))
68100 (COND(FLG(SETQ SAVEED(CDR STRAT))(SETQ SAVESTR(CAR STRAT))))
68200 (SETQ XYZ1 XX)
68300 (COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
68400 (PRINT SETQMESS)
68500 (SETQ XX (UPDATE XX))
68600 (SETQ XYZ1 XX)
68700 SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
68800 (PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
68900 AA (CLAUSES XX)
69000 SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
69100 (AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
69200 (COND
69300 ((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
69400 SR2A (PRINT (QUOTE THE-FOLLOWING-BUILTIN-STRATEGIES-ARE-AVAILABLE:))
69500 (PRINT
69600 (QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1
69700 SUPPORT[#,..] EQUALITY[ID,#] "))
69800 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
69900 (COND
70000 (FLG (OUTIT SAVESTR)
70100 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
70200 (SETQ Z (READ))
70300 (COND ((EQ Z (QUOTE N)) (GO SRB)))))
70400 (SCANSET)
70500 (START)
70600 (SETQ Z (ERRSET (<ST>) T))
70700 (SCANRESET)
70800 (COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SR2A)))
70900 (SETQ SAVESTR(SETQ ZIN (TOP)))
71000 (OUTIT ZIN)
71100 SRB (SETQ DEBUG T)
71200 SRAA (PRINT (QUOTE EDIT-STRATEGY-IS:))
71300 (COND
71400 (FLG (OUTIT SAVEED)
71500 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
71600 (SETQ Z (READ))
71700 (COND ((EQ Z (QUOTE N)) (GO SRCA)))))
71800 (SCANSET)
71900 (START)
72000 (SETQ Z1 (ERRSET (<ST>) T))
72100 (SCANRESET)
72200 (COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
72300 (SETQ SAVEED (SETQ ZIN (TOP)))
72400 (OUTIT ZIN)
72500 SRCA (SETQ UFLG T)
72600 (SETQ Z1
72700 (CONS SAVESTR SAVEED))
72800 (OUTC CHAN NIL)
72900 (COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
73000 EXPR)
73100
73200 (DEFPROP SETSUP
73300 (LAMBDA(X)
73400 (PROG (Z)
73500 (SETQ X (*CL X CLAUSES))
73600 A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
73700 (SETQ Z (CONS (CDAR X) Z))
73800 (SETQ X (CDR X))
73900 (GO A)))
74000 EXPR)
74100
74200 (DEFPROP SUBS3TA
74300 (LAMBDA(L Z XX TS)
74400 (PROG (X1 X2 X3 Z4)
74500 (SETQ X1 (LIST (CAR Z)))
74600 (SETQ X2 X1)
74700 (GO SUB2)
74800 SUB1 (RPLACD X2 (LIST X3))
74900 (SETQ X2 (CDR X2))
75000 SUB2 (SETQ Z (CDR Z))
75100 (SETQ Z4 (CAR Z))
75200 (COND ((NULL Z) (RETURN X1))
75300 ((EQ Z XX) (SETQ X3 TS) (GO SUB1))
75400 ((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
75500 ((CONST Z4) (SETQ X3 Z4) (GO SUB1))
75600 (T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
75700 EXPR)
75800
75900 (DEFPROP SUBS3T**
76000 (LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
76100 EXPR)
76200
76300 (DEFPROP SUB*
76400 (LAMBDA(X L)
76500 (PROG (S2 Z L1)
76600 B (SETQ L1 L)
76700 A (SETQ S2 (CDADAR L1))
76800 (SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
76900 (COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
77000 (SETQ L1 (CDR L1))
77100 (COND (L1 (GO A)))
77200 (SETQ X (CDR X))
77300 (COND (X (GO B)))))
77400 EXPR)
77500
77600 (DEFPROP SUBSKOL
77700 (LAMBDA (C EXL) (SUBS3T EXL C))
77800 EXPR)
77900
78000 (DEFPROP SUPPORT
78100 (LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
78200 EXPR)
78300
78400 (DEFPROP SUBSUME1
78500 (LAMBDA(C CB D DB L)
78600 (PROG (Z)
78700 SUB5 (COND ((NEG (CAR C)) (GO SUB3))
78800 ((NEG (CAR D)) (RETURN NIL))
78900 ((EQ (CAAR C) (CAAR D)) (GO SUB1))
79000 ((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
79100 (T (GO SUB2)))
79200 SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
79300 SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
79400 SUB2 (SETQ D (CDR D))
79500 (COND (D (SETQ DB (CDR DB)) (GO SUB5)))
79600 (RETURN NIL)
79700 SUB3 (COND
79800 ((NEG (CAR D))
79900 (COND ((EQ (CADAR C) (CADAR D))
80000 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
80100 (T (GO SUB2))))
80200 ((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
80300 (T (GO SUB2)))))
80400 (SETQ D (CDR D))
80500 (COND (D (SETQ DB (CDR DB)) (GO SUB3)))
80600 (RETURN NIL)))
80700 EXPR)
80800
80900 (DEFPROP SUBS2T
81000 (LAMBDA(X Y Z)
81100 (PROG (U Z1)
81200 (COND ((EQ X Y) (RETURN Z)))
81300 (SETQ U (CDR Z))
81400 (GO S2)
81500 S1 (SETQ Z1 (CDAR U))
81600 (COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
81700 ((CONST Z1) NIL)
81800 (T (RPLACD (CAR U) (S2 X Y Z1))))
81900 (SETQ U (CDR U))
82000 S2 (COND (U (GO S1)))
82100 (RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
82200 (RETURN Z)))
82300 EXPR)
82400
82500 (DEFPROP SUBS3T
82600 (LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
82700 EXPR)
82800
82900 (DEFPROP SUBSUME
83000 (LAMBDA(C D)
83100 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
83200 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
83300 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
83400 (T NIL)))
83500 EXPR)
83600
83700
83800 (DEFPROP SUBST1
83900 (LAMBDA(X Y Z)
84000 (COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
84100 ((EQUAL Y Z) X)
84200 (T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
84300 EXPR)
84400
84500 (DEFPROP TCOPY
84600 (LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
84700 EXPR)
84800
84900 (DEFPROP TERMS
85000 (LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
85100 EXPR)
85200
85300 (DEFPROP TERMS1
85400 (LAMBDA(L N)
85500 (COND ((OR (ZEROP N) (NULL L)) NIL)
85600 ((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
85700 (T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
85800 EXPR)
85900
86000 (DEFPROP TERMS2
86100 (LAMBDA(Z L N)
86200 (PROG (Z1 T1 T2)
86300 (SETQ T2 (SETQ T1 (LIST NIL)))
86400 A (COND ((NULL L) (RETURN T1))
86500 ((VAR (CAR L)) (GO B))
86600 ((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
86700 ((EQ N 1) (GO B)))
86800 (SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
86900 (COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
87000 (COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
87100 B (SETQ L (CDR L))
87200 (GO A)))
87300 EXPR)
87400
87500 (DEFPROP TIMEIT
87600 (LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
87700 EXPR)
87800
89100
89200 (DEFPROP TRY
89300 (LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
89400 FEXPR)
89500
89600 (DEFPROP TRY1
89700 (LAMBDA(L)
89800 (PROG (
89850 ITER PREFN EQUAL INFN INFPREDLET IVAR PREPREDLET FNNO FNNAM
89862 VARTBL OUTVAR VARNO
89875 FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
89887 (SETQ INFN @(%))(SETQ FNNO 0)(SETQ FNNAM @AXIOM)
89893 (SETQ VARNO 1)
89900 (SETQ ITER(SETQ PRNO 0))
90000 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
90100 (SETQ Z (CAR (LAST L)))
90200 (SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
90300 (EVAL (CONS (QUOTE INPUT) L))
90400 (INC T)
90500 P3 B (SETQ Z2 (INCLAUSES))
90600 (INC NIL)
90700 (COND ((NULL Z2) (RETURN NIL)))
90800 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
90900 (SETQ Z2 (ATTEMPT Z2 NIL NIL))
91000 A (COND ((OR (NULL Z2) (EQ (CAR Z2) (QUOTE QED))) (RETURN (QUOTE *)))
91100 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
91200 ((EQ (CAR Z2) (QUOTE ABORT))
91300 (SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
91400 (GO A)))
91500 FEXPR)
91600
91700 (DEFPROP TRYIT
91800 (LAMBDA NIL
00100 (PROG (Z1 Z2 R M)
00200 (SETQ CNT (ADD1 (LENGTH CLAUSES)))
00300 (SETQ EE (CDR EE))
00400 TRY3 (SETQ Z1 (CAR EE))
00500 (COND ((NOT (HERE Z1)) (GO TRY7)))
00600 (SETQ M (CHOICE Z1))
00700 (COND ((NULL M) (GO TRY7)))
00800 TRY2 (SETQ Z2 (CAR M))
00900 (COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
01000 TRY1 TRY1A
01100 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
01200 (SETQ R (RESOLVE Z1 Z2))
01300 (COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
01400 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
01500 TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
01600 (SETQ R (PARMOD Z1 Z2))
01700 (COND ((NULL R) (GO TRY8)))
01800 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
01900 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
02000 (SETQ M (CDR M))
02100 (COND (M (GO TRY2)))
02200 TRY7 (SETQ EE (CDR EE))
02300 (COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
02400 (PRINT (QUOTE COUNT))
02500 (PRINT COUNT)
02600 (PRINT (QUOTE LEVEL))
02700 (PRINT LVL)
02800 (SETQ LVL (ADD1 LVL))
02900 (PRINT (QUOTE ELAPSED-TIME))
03000 (PRINT (TIMEIT))
03100 (COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03200 (PRINT (QUOTE NO-PROOF-FOUND))
03300 (COND (AUTO (ERR (QUOTE NOPROOF))))
03400 (UPDATE CLAUSES)
03500 (COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03600 (ERR (QUOTE NOPROOF))))
03700 EXPR)
03800
03900 (DEFPROP TRAVERSE
04000 (LAMBDA(L)
04100 (PROG (Z Z1 Z2)
04200 (SETQ Z (ANCESTOR L))
04300 (SETQ Z1 (CAR Z))
04400 (SETQ Z (CDR Z))
04500 (COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
04600 (COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
04700 (RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
04800 EXPR)
04900
05000 (DEFPROP UNIT
05100 (LAMBDA (X) (EQ (NUM X) 1))
05200 EXPR)
05300
05400 (DEFPROP UNITS
05500 (LAMBDA(U)
05600 (PROG (Z Z1)
05700 (COND ((NULL U) (RETURN NIL)))
05800 (SETQ Z U)
05900 UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
06000 (SETQ Z (CDR Z))
06100 (COND (Z (GO UN1)))
06200 (RETURN Z1)))
06300 EXPR)
06400
06500 (DEFPROP UNITRES
06600 (LAMBDA(C UP UN)
06700 (PROG (C1 Z1 U Z RES)
06800 (SETQ C1 C)
06900 (COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
07000 (COND
07100 ((UNIT C)
07200 (RETURN
07300 (COND ((ALLPOS C) (RESUNITP (CAADR C) (CDADR C) UN)) (T (RESUNITN (CADADR C) (CDDADR C) UP))))))
07400 (COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
07500 (SETQ C (CDR C))
07600 B (SETQ Z1 (CAR C))
07700 (COND ((NEG Z1) (GO N)))
07800 (SETQ U UN)
07900 A (COND ((NOT (EQ (CAR Z1) (CADADR (CAR U)))) (GO A1)))
08000 (SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
08100 (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
08200 (SETQ RES (CONS (REDUCER C1 C) RES))
08300 (GO A2)
08400 A1 (SETQ U (CDR U))
08500 (COND (U (GO A)))
08600 A2 (SETQ C (CDR C))
08700 (COND (C (GO B)) (T (RETURN RES)))
08800 N (SETQ Z1 (CDAR C))
08900 (SETQ U UP)
09000 C (COND ((NULL U) (RETURN RES)))
09100 C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
09200 (SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
09300 (COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
09400 (SETQ RES (CONS (REDUCER C1 C) RES))
09500 (GO C3)
09600 C1 (SETQ U (CDR U))
09700 (COND (U (GO C2)))
09800 C3 (SETQ C (CDR C))
09900 (COND (C (GO N)) (T (RETURN RES)))))
10000 EXPR)
10100
10200 (DEFPROP UNITREDUCT
10300 (LAMBDA(R UP UN)
10400 (PROG (Z UP1 UN1 C1 C2 RC1 RC2)
10500 (SETQ UN1 (SETQ UP1 NIL))
10600 (SETQ C1 (SETQ C2 R))
10700 A (SETQ RC1 (SETQ RC2 NIL))
10800 (COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
10900 B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
11000 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
11100 ((NULL (CAR Z)) (RETURN (LIST NIL)))
11200 (T (SETQ RC1 (APPEND Z RC1))))
11300 (SETQ C2 (CDR C2))
11400 (COND (C2 (GO B)))
11500 C1 (SETQ UP (APPEND UP1 UP))
11600 (SETQ UN (APPEND UN1 UN))
11700 C (SETQ Z (UNITRES (CAR C1) UP UN))
11800 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
11900 ((NULL (CAR Z)) (RETURN (LIST NIL)))
12000 (T (SETQ RC1 (APPEND Z RC1))))
12100 (SETQ C1 (CDR C1))
12200 (COND (C1 (GO C)))
12300 (COND ((NULL RC1) (RETURN RC2)))
12400 (SETQ C2 RC2)
12500 (SETQ C1 RC1)
12600 (SETQ Z (UNITPN C1))
12700 (COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
12800 (SETQ UP1 (CAR Z))
12900 (SETQ UN1 (CDR Z))
13000 (GO A)))
13100 EXPR)
13200
13300 (DEFPROP UNITPN
13400 (LAMBDA(X)
13500 (PROG (P N)
13600 A (COND
13700 ((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
13800 (SETQ X (CDR X))
13900 (COND (X (GO A)))
14000 (RETURN (CONS P N))))
14100 EXPR)
14200
14300 (DEFPROP UNIFY
14400 (LAMBDA(X Y)
14500 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
14600 (SETQ LC (LIST NIL))
14700 U3 (SETQ Z1 (CAR X))
14800 (SETQ Z2 (CAR Y))
14900 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
15000 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
15100 (COND ((VAR Z3)
15200 (COND ((VAR Z4) (GO UN1))
15300 ((CONST Z4) (GO UN3))
15400 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
15500 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
15600 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
15700 ((VAR Z4)
15800 (COND ((CONST Z3) (GO UN1))
15900 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
16000 ((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
16100 (COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
16200 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
16300 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
16400 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
16500 (SETQ X (APPEND Z6 (CDR X)))
16600 (SETQ Y (APPEND Z7 (CDR Y)))
16700 (GO U3))
16800 (T (RETURN NIL)))
16900 UN1 (SUBS2T Z3 Z4 LC)
17000 UN2 (SETQ X (CDR X))
17100 (COND (X (SETQ Y (CDR Y)) (GO U3)))
17200 (RETURN LC)
17300 UN3 (SUBS2T Z4 Z3 LC)
17400 (GO UN2)))
17500 EXPR)
17600
17700 (DEFPROP UNI
17800 (LAMBDA(C D L)
17900 (PROG (Z1 Z2 Z3)
18000 UN2 (SETQ Z2 (CAR D))
18100 (SETQ Z1 (SETQ Z3 (CAR C)))
18200 (COND
18300 ((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
18400 (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
18500 ((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
18600 (COND ((VAR Z2) (RETURN NIL))
18700 ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
18800 ((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
18900 ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
19000 (SETQ D (APPEND (CDR Z2) (CDR D)))
19100 (GO UN2))
19200 (T (RETURN NIL)))
19300 UN1 (SETQ C (CDR C))
19400 (COND (C (SETQ D (CDR D)) (GO UN2)))
19500 (COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
19600 EXPR)
19700
19800 (DEFPROP UNION
19900 (LAMBDA(Z C D YC YD)
20000 (PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
20100 (SETQ NO* NO)
20200 (COND
20300 (ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
20400 (COND ((< L (CDR SAT)) (RETURN NIL)))))
20500 (SETQ M1 0)
20600 (SETQ Z7 (ANCESTOR C))
20700 (SETQ Z8 (ANCESTOR D))
20800 (SETQ C (CDR C))
20900 (SETQ D (CDR D))
21000 (SETQ Z1 Z)
21100 (SETQ Z2 Z)
21200 (SETQ Z3 (SUBS3T** Z1 YC))
21300 (SETQ Z4 (SUBS3T** Z2 YD))
21400 UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
21500 (COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
21600 ((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
21700 (SETQ C1 (CONS Z5 C1))
21800 UN1A (SETQ C (CDR C))
21900 (COND (C (GO UN1)))
22000 UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
22100 (COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
22200 ((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
22300 ((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
22400 ((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
22500 UN2B (SETQ C2 (CONS Z6 C2))
22600 UN2A (SETQ D (CDR D))
22700 (COND (D (GO UN2)))
22800 (SETQ Z2 0)
22900 (COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
23000 ((NULL C2) (SETQ Z1 C1) (GO UN7)))
23100 (COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
23200 UN5 (SETQ NEG RES)
23300 (COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
23400 ((NULL C2) (SETQ Z1 C1) (GO UN7))
23500 ((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
23600 ((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
23700 ((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
23800 (SETQ Z1 (CAR C1))
23900 (SETQ C1 (CDR C1))
24000 (GO UN4)))
24100 UN6 (SETQ Z1 (CAR C2))
24200 (SETQ C2 (CDR C2))
24300 UN4 (UPIT Z1)
24400 (COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
24500 UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
24600 (SETQ Z2 (ADD1 Z2))
24700 (UPIT (CAR Z1))
24800 (SETQ RES (CONS (CAR Z1) RES))
24900 (COND ((NEG (CAR Z1)) (SETQ NEG RES)))
25000 UN8 (SETQ Z1 (CDR Z1))
25100 (GO UN7)
25200 UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
25300 (SETQ Z1 (CAR C2))
25400 (SETQ C2 (CDR C2))
25500 UN4A (UPIT1 (CDR Z1))
25600 (COND ((MEMBER Z1 RES) (GO UN5A)))
25700 (SETQ Z2 (ADD1 Z2))
25800 (SETQ RES (CONS Z1 RES))
25900 UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
26000 (GO UN3)))
26100 EXPR)
26200
26300 (DEFPROP UNWIND
26400 (LAMBDA(X1 X2 Y Z N)
26500 (PROG (Z1 Z2)
26600 (SETQ Z2 (ASSOC1 X1 Z))
26700 (COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
26800 (NCONC Y (COPYDELETED X1))
26900 (NCONC Z (LIST (CONS (LAST Y) N)))
27000 (SETQ Z1 N)
27100 (SETQ N (ADD1 N))
27200 A (SETQ Z2 (ASSOC1 X2 Z))
27300 (COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
27400 (NCONC Y (COPYDELETED X2))
27500 (NCONC Z (LIST (CONS (LAST Y) N)))
27600 (RETURN (CONS (CONS Z1 N) (ADD1 N)))))
27700 EXPR)
27800
27900 (SPECIAL E)
28000 (DEFPROP UPDATE
28100 (LAMBDA(E)
28200 (PROG (USINGFL USING
28300 CHAN1
28400 ELOC
28500 CHAN
28600 AUTO
28700 DL1
28800 RF
28900 XYZ
29000 XYZ1
29100 CMD
29200 LOCFLG
29300 Z
29400 Z1
29500 Z2
29600 INCT
29700 Z3
29800 Z1R
29900 Z2R
30000 N1
30100 R
30200 N
30300 NAME
30400 NAMELIST
30500 ZZ)
30600 (SETQ CHAN (OUTC NIL NIL))
30700 (SETQ AXNO (QUOTE INSERT))
30800 (SETQ FNNAM (QUOTE EDI))
30900 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
31000 (SETQ N1 (LAST NAMELIST))
31100 (SETQ INCT (INC NIL))
31200 U9 (SETQ ELOC E)
31300 (SETQ N 1)
31400 U3 (UP1A (CAR ELOC) N)
31500 U3A (TERPRI)
31600 U3AA (SETQ CMD (READ))
31700 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
31800 U3B (COND ((NOT (ATOM CMD)) (GO UER2)))
31900 U3C (SETQ CMD (EXPLODE CMD))
32000 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
32100 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
32200 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
32300 (GO U3A)
32400 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
32500 (GO U3A)
32600 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
32700 (COND ((NULL Z1) (GO U3A)))
32800 (CLAUSES Z1)
32900 (GO U3A)
33000 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
33100 (SETQ Z NAMELIST)
33200 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
33300 (SETQ Z (CDR Z))
33400 (COND (Z (GO USY2)))
33500 (GO U3A)
33600 UFL2 (SETQ Z (QUOTE U))
33700 (GO UFL4)
33800 UFL3 (SETQ Z (QUOTE D))
33900 (GO UFL4)
34000 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
34100 UFL4 (SETQ Z2 405104)
34200 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
34300 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
34400 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
34500 (UPDATESTATE (CDDR Z))
34600 (GO U3A)
34700 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
34800 (COND ((NULL Z2) (GO U3A)))
34900 (EXPUNGE Z2)
35000 (GO U3A)
35100 UIN1 (SETQ NAME (READ))
35200 (SETQ Z2 (UPGETL E NAMELIST))
35300 (COND ((NULL Z2) (GO U3A)))
35400 UIN1A
35500 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
35600 (NCONC Z1 Z2)
35700 (GO U3A)
35800 USU1 (SETQ Z1 (ERRSET (GETTERMS E NAMELIST)))
35900 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
36000 ((NULL (CAR Z1)) (GO U3A)))
36100 (SETQ Z3 NIL)
36200 (SETQ Z1 (CAR Z1))
36300 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
36400 (SETQ Z1 (CDR Z1))
36500 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2(SET3 (SETUP Z3))) (GO UIN1A)))
36600 UUP1 (SETQ Z2 (READ))
36700 (COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U8)) (T (GO UER2)))
36800 UDO1 (SETQ Z2 (READ))
36900 (COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U7)) (T (GO UER2)))
37000 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
37100 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
37200 (SETQ Z2 (CDR Z2))
37300 (GO UAN2)
37400 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
37500 (INC INCT)
37600 (OUTC CHAN NIL)
37700 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
37800 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
37900 (RETURN (MINIMIZE (APPEND Z1 Z)))
38000 USA1 (SETQ Z2 (UPGETL E NAMELIST))
38100 (COND (Z2 (NCONC E Z2)))
38200 (GO U3A)
38300 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
38400 (SETQ Z2 (UPGETL E NAMELIST))
38500 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
38600 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
38700 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
38800 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
38900 (SETQ Z3 Z1)
39000 (SETQ Z DDEPTH)
39100 (SETQ DDEPTH 22)
39200 USI2 (DEMOD (LIST (CAR Z3)) Z2)
39300 (SETQ Z3 (CDR Z3))
39400 (COND (Z3 (GO USI2)))
39500 (PRINT (QUOTE CLAUSES-ARE:))
39600 (CLAUSES Z1)
39700 (SETQ DDEPTH Z)
39800 (GO U3A)
39900 UCU1 (QUERY)
40000 (GO U3A)
40100 UDS1 (SETQ Z1 (READ))
40200 (COND ((NOT (ATOM Z1)) (GO UDS3)))
40300 UDS2 (COND
40400 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
40500 (GO UDS2)))
40600 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
40700 (GO U3A)
40800 UEO1 (OUTC CHAN1 T)
40900 (GO U3A)
41000 UUS1 (SETQ NAME (QUOTE %USING))
41100 (SETQ USINGFL T)
41200 (SETQ USING NIL)
41300 UUS3 (SETQ LOCFLG T)
41400 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
41500 (SETQ USINGFL NIL)
41600 (COND ((NULL Z2) (GO U3A)))
41700 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
41800 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
41900 (T (RPLACA (CAR N1) NAME)
42000 (RPLACD (CAR N1) Z2)
42100 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
42200 (SETQ N1 (CDR N1))))
42300 (GO U3A)
42400 USE1 (SETQ NAME (READ))
42500 (SETQ LOCFLG NIL)
42600 (GO UUS2)
42700 UCL1 (SETQ Z (READ))
42800 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
42900 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
43000 (GO UCL2))
43100 (T (GO U3A)))
43200 UGO1 (SETQ Z1 (READ))
43300 (COND ((NOT (NUMBERP Z1)) (GO UER2)))
43400 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
43500 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
43600 UTR1 (SETQ AUTO NIL)
43700 (GO UEX2)
43800 UEX1 (SETQ AUTO T)
43900 UEX2 (SETQ NAME (QUOTE LEMMA))
44000 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
44100 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
44200 (SETQ Z2
44300 (ATTEMPT (INITIALAX (CONS THEOREMNAME (APPEND XYZ USING)))
44400 NIL
44500 NIL))
44600 (GO AT1A)
44700 UST1 (STOP)
44800 (GO U3A)
44900 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
45000 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
45100 U8 (COND ((EQ Z2 0) (GO U9)))
45200 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
45300 (SETQ Z2 (DIFFERENCE Z2 5))
45400 (SETQ ZZ 5)
45500 U84 (SETQ Z N)
45600 (SETQ Z3 (DIFFERENCE N ZZ))
45700 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
45800 (SETQ N Z3)
45900 (SETQ Z3 ELOC)
46000 (SETQ ELOC (DOWN N E))
46100 (SETQ ZZ NIL)
46200 (SETQ Z1 ELOC)
46300 U81 (COND ((EQ Z1 Z3) (GO U82)))
46400 (SETQ ZZ (CONS (CAR Z1) ZZ))
46500 (SETQ Z1 (CDR Z1))
46600 (GO U81)
46700 U82 (COND ((NULL ZZ) (GO U83)))
46800 (UP1A (CAR ZZ) (SUB1 Z))
46900 (SETQ ZZ (CDR ZZ))
47000 (SETQ Z (SUB1 Z))
47100 (GO U82)
47200 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
47300 (SETQ Z2 (PLUS Z2 N))
47400 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
47500 (SETQ ELOC (CDR ELOC))
47600 (SETQ N (ADD1 N))
47700 (UP1A (CAR ELOC) N)
47800 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
47900 UPR1 (TERPRI)
48000 (SETQ XYZ NIL)
48100 (SETQ Z2 (UPGETL E NAMELIST))
48200 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
48300 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
48400 (SETQ AXNO THEOREMNAME)
48500 (SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
48600 (SETQ AXNO (QUOTE INSERT))
48700 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
48800 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
48900 (SETQ NAME (QUOTE LEMMA))
49000 (SETQ LOCFLG T)
49100 (GO USE2)
49200 UME1 (SETQ Z1 (UPGETL E NAMELIST))
49300 (SETQ Z2 (UPGETL E NAMELIST))
49400 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
49500 (BAKSUB Z1 Z2)
49600 (GO U3A)
49700 UHE1 (PRINT MESSAGE)
49800 (GO U3A)
49900 URE1 (SETQ Z1 (UPGETL E NAMELIST))
50000 (SETQ Z2 (UPGETL E NAMELIST))
50100 U%RE1
50200 (SETQ RF T)
50300 URE1A
50400 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
50500 (SETQ Z1R Z1)
50600 (SETQ Z2R Z2)
50700 (SETQ Z3 NIL)
50800 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
50900 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
51000 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
51100 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
51200 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
51300 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
51400 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
51500 UR3A (SETQ Z2R (CDR Z2R))
51600 (COND (Z2R (GO UR3)))
51700 (SETQ Z1R (CDR Z1R))
51800 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
51900 UR3B (COND ((NULL Z3)
52000 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
52100 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
52200 (RF (SETQ NAME (QUOTE RES)))
52300 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
52400 (SETQ Z2 Z3)
52500 (SETQ LOCFLG T)
52600 (GO AT2A)
52700 UEV1 (PRINT (QUOTE EVAL-AWAITS))
52800 (SETQ Z2 (ERRSET (EVAL (READ)) T))
52900 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
53000 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
53100 (GO UEV1)
53200 AT1A (UPDATESTATE STRAT)
53300 (COND
53400 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
53500 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
53600 (PRINC NAME)
53700 (GO U3A))
53800 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
53900 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
54000 (SETQ AUTO NIL)
54100 (GO AT1A))
54200 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
54300 (SETQ Z2 (CADR Z2))
54400 AT2A (SETQ N 1)
54500 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
54600 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
54700 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
54800 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
54900 (PRIN1 NAME)
55000 (CLAUSES Z2)
55100 (GO USE2)))
55200 EXPR)
55300
55400 (UNSPECIAL E)
55500 (DEFPROP UPGETL
55600 (LAMBDA(E N)
55700 (PROG (C)
55800 (SCANSET)
55900 (START)
56000 (SETQ C (ERRSET (<CLAUSES>) T))
56100 (SCANRESET)
56200 (COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
56300 (SETQ C (TOP))
56400 (COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
56500 (RETURN (UPGETL1 C E N))))
56600 EXPR)
56700
56800 (DEFPROP UPGETL1
56900 (LAMBDA(C E N)
57000 (PROG (N1 Z Z1 Z2 Z3 ZZ N2)
57100 AS1 (SETQ Z (CAR C))
57200 (COND ((ATOM Z)
57300 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
57400 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
57500 (T (RETURN NIL))))
57600 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
57700 (T (RETURN NIL))))
57800 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
57900 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
58000 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
58100 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
58200 (T (RETURN NIL)))
58300 AS6 (SETQ C (CDR C))
58400 (COND (C (GO AS1)) (T (RETURN ZZ)))
58500 AS2 (SETQ Z2 (CADR Z))
58600 (SETQ N1 (CAR Z))
58700 (SETQ Z (CDR Z))
58800 (SETQ Z3 Z1)
58900 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
59000 AS3 (SETQ Z2 (SUB1 Z2))
59100 (COND ((ZEROP Z2) (GO AS4)))
59200 (SETQ Z1 (CDR Z1))
59300 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
59400 AS4 (COND
59500 ((NOT (HERE (CAR Z1))) (PRINT N1)
59600 (PRINC (QUOTE / ))
59700 (PRINC (CAR Z))
59800 (PRINC (QUOTE / ))
59900 (PRINC (QUOTE HAS-BEEN-DELETED))
60000 (RETURN NIL)))
60100 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
60200 (SETQ Z (CDR Z))
60300 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
60400 (GO AS6)
60500 AS10 (SETQ N2 (QUOTE INSERT))
60600 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF(COPY (SETQ XYZ (FIXQFF (CDR Z)))))))))
60700 (GO AS6)
60800 AS20 (SETQ N2 (QUOTE MATCHES))
60900 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
61000 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
61100 AS30 (SETQ N2 (QUOTE INPUT))
61200 (SETQ ZIN (CDR Z))
61300 (COND
61400 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
61500 (INC T)
61600 (SETQ Z (INCLAUSES))
61700 (INC NIL)
61800 (COND ((NULL Z) (RETURN NIL)))
61900 AS31 (SETQ ZZ (APPENDIT ZZ Z))
62000 (GO AS6)))
62100 EXPR)
62200
62300
62400 (DEFPROP UPDATESTATE
62500 (LAMBDA(L)
62600 (PROG NIL
62700 (SETQ STRATEGY(BUILTCH(CAR L)))
62800 (SETQ EDITSTRAT(BUILTED(CDR L)))
62850 (SETQ STRAT L)
62900 ))
63000 EXPR)
63100
63200 (DEFPROP UPIT
63300 (LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
63400 EXPR)
63500
63600 (DEFPROP UPIT1
63700 (LAMBDA(Z)
63800 (PROG (Z1 Z2)
63900 MAX2 (SETQ Z2 (CAR Z))
64000 (COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
64100 ((GREATERP Z2 NO*) NIL)
64200 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
64300 (GO MAX1))
64400 ((CONST Z2) (GO MAX1))
64500 (T (UPIT1 (CDR Z2))))
64600 MAX1 (SETQ Z (CDR Z))
64700 (COND (Z (GO MAX2)))
64800 (RETURN NO)))
64900 EXPR)
65000
65100 (DEFPROP UP1A
65200 (LAMBDA(X N)
65300 (PROG NIL
65400 (TERPRI)
65500 (PRINC N)
65600 (PRINC (QUOTE / ))
65700 (COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
65800 (RETURN NIL)))
65900 EXPR)
66000
66100 (DEFPROP UP1B
66200 (LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
66300 EXPR)
66400
68000
68100 (DEFPROP VINE
68200 (LAMBDA (X) (ATOM (CDR (ANCESTOR X))))
68300 EXPR)
68400
68500 (DEFPROP <
68600 (LAMBDA(L X)
68700 (PROG (Z Z1 Z2)
68800 (SETQ Z X)
68900 (COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
69000 A1 (SETQ Z1 (CAR Z))
69100 (COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
69200 (COND ((NOT (ORDERP L Z1)) (GO A2))
69300 ((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
69400 A2 (SETQ Z (CDR Z))
69500 (COND (Z (GO A1)))
69600 (RETURN NIL)))
69700 EXPR)
69800
69900 (DE MAXLENGTH(X N)(GREATERP (NUM X) N))
70000
70100
70200 (DEFPROP MAXDEPTH
70300 (LAMBDA(Z N)
70400 (PROG NIL
70500 D1 (COND ((MAXDEPTH1 (COND ((NEG (CAR Z)) (CDDAR Z)) (T (CDAR Z))) N) (RETURN T)))
70600 (SETQ Z (CDR Z))
70700 (COND (Z (GO D1))) (RETURN NIL)))
70800 EXPR)
70900
71000 (DEFPROP MAXDEPTH1
71100 (LAMBDA(Z N)
71200 (PROG NIL
71300 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2))
71400 ((EQ N 1) (RETURN T))
71500 ((MAXDEPTH1 (CDAR Z) (SUB1 N)) (RETURN T)))
71600 D2 (SETQ Z (CDR Z))
71700 (COND (Z (GO D1)))
71800 (RETURN NIL)))
71900 EXPR)
00100
00200
00300 (DEFPROP DEP
00400 (LAMBDA(L)
00500 (PROG (C1 C2)
00600 (SETQ C1 (CDR C))
00700 A (SETQ C2 (COND ((NEG (CAR C1)) (CDDAR C1)) (T (CDAR C1))))
00800 (COND ((DEP1 C2 (COPY L)) (RETURN T)))
00900 (SETQ C1 (CDR C1))
01000 (COND (C1 (GO A)))
01100 (RETURN NIL)))
01200 FEXPR)
01300
01400 (DEFPROP DEP1
01500 (LAMBDA(C L1)
01600 (PROG (L Z)
01700 A(SETQ L (COPY L1)) (COND ((VAR (CAR C)) (GO B)))
01800 (SETQ Z (ASSOC (CAAR C) L))
01900 (COND ((NULL Z) NIL) ((EQ (CDR Z) 1) (RETURN T)) (T (RPLACD Z (SUB1 (CDR Z)))))
02000 (COND ((NULL (CDAR C)) NIL) ((DEP1 (CDAR C) L) (RETURN T)))
02100 B (SETQ C (CDR C))
02200 (COND (C (GO A)))
02300 (RETURN NIL)))
02400 EXPR)